2 Predicate Logic
Predicate logic extends propositional logic allowing to reason about whole classes of entities.
Predicate logic assumes the world contains objects. Objects are represented with variables. The relations between objects are specified with predicates.
A predicate is an expression involving one or more variables. It is a template that specifies a property of objects, or a relation among objects. Substitution of a particular value for the variables produces a proposition that is either true or false.
A variable has a domain, the set of all values that may be substituted in place of the variable. The n-arity define the number of variable of a predicate.
Predicate logic introduces two new operator called quantifiers: \forall (universal quantifier) and \exists (existential quantifier).
2.1 Syntax of Predicate Logic
There are two kind of legal expressions in predicate logic: terms and formulas. Terms are objects. Formulas express predicates that can be evaluated to true or false.
Terms are defined as follows:
Any variable is a term
Any constant (nullary function) is a term
If t_1, t_2, …, t_n are terms and f is a n-ary function, then f(t_1, t_2, …, t_n) is a term.
Function symbols are denoted by lowercase letters.
A well-formed formula is inductively defined as
If P is an n-ary predicate symbol and t_1, …, t_n are terms, then P(t_1, …, t_n) is a formula
If the equality symbol is part of logic, and t_1 and t_2 are terms, then t_1 = t_2 is a formula. The equality cannot be used between two formulas.
If \varphi is a formula, then so is (\neg \varphi)
If \varphi and \psi are formulas, then so are (\varphi \land \psi), (\varphi \lor \psi) and (\varphi \rightarrow \psi)
If \varphi is a formula and x is a variable, then (\forallx \varphi) and (\existsx \varphi) are formulas.
Formulas obtained from the first two rules are called atomic formulas.
\neg is evaluated first
\forallx and \existsy are evaluated next
\land and \lor are evaluated after
\rightarrow is evaluated last
In the parse tree of a well-formed predicate logic formula there are three new types of nodes:
The quantifiers \forallx and \existsy form nodes that have one subtree
Any predicate of n-ary P(t_1, t_2, …, t_n) has the symbol P as a node and the node has a subtree for each of the terms t_1, …, t_n
Any function of n-ary f(t_1, t_2, …, t_n) has the symbol f as a node and the node has a subtree for each of the terms t_1, …, t_n
2.2 Free and bound variables
All variables that are not quantified in a formula are free variables, those quantified are bound variables.
They are defined inductively as follows:
There are no bound variables in any atomic formula
x is free in \neg \varphi if and only if x is free in \varphi. x is bound in \neg \varphi if and only if x is bound in \varphi
x occurs free in \varphi \land \psi if and only if x occurs free in either \varphi or \psi. x occurs bound in (\varphi \land \psi) if and only if x occurs bound in either \varphi or \psi. The same rule applies to the other two binary connectives
x is free in \forally \varphi if and only if x is free in \varphi and x is a different symbol free from y. Also, x is bound in \forally \varphi if and only if x is y or x is bound in \varphi. The same rule applies to \exists.
Free and bound variables can be determined through a parse tree: choose a leaf node for an occurrence of a variable and walk up the tree, if a quantifier for the variable is encountered, then this occurrence of variable is bound.
A well-formed predicate logic formula that contains no free variables is said to be closed.
2.3 Substitution
Let \varphi be a formula, x a variable, and t a term. Replace each free occurrence of x in \varphi with t and denote the new formula by \varphi[t/x].
Given a term t, a variable x, and a formula \varphi, we say that t is free for x in \varphi if no free x in \varphi occurs in the scope of \forally or \existsy for any variable y occurring in t. It is safe to substitute t for x in \varphi if t is free for x in \varphi.
Formally, for a formula \varphi:
If φ is P(t₁, t₂, …, tₖ), then φ[t/x] is P(t₁[t/x], t₂[t/x], …, tₖ[t/x]).
If φ is (¬φ₁), then φ[t/x] is (¬φ₁[t/x]).
If φ is (φ₁ ∧ φ₂), then φ[t/x] is (φ₁[t/x] ∧ φ₂[t/x]). This also applies to (φ₁ ∨ φ₂) and (φ₁ → φ₂).
If φ is (∀x φ₁) or (∃x φ₁), then φ[t/x] is φ.
If φ is (∀y φ₁) or (∃y φ₁), then
If y does not occur in t, then φ[t/x] is (∀y φ₁[t/x]) or (∃y φ₁[t/x]), respectively.
Otherwise, we select a variable z that occurs in neither φ nor t to replace all y first, and then we substitute x with t.
2.4 Skolemization
Allows the elimination of existential quantifiers: given as example ∀y ∃x P(x, y) the dependence of x on y may be expressed by a Skolem function g(y): \forally P(g(y), y). If the existential quantifier to be eliminated is not in the scope of any universal quantifier a constant is used.
Symbols in Skolem functions must be fresh (not already appearing in the formula).
2.5 Deduction rules
The propositional logic deduction rules are all valid.
Here we introduce rules added by the new operators:
Equality introduction: \dfrac{}{t = t} = i
Equality elimination: \dfrac{t_1 = t_2, \varphi[t_1/x]}{\varphi[t_2/x]} = e
\forallx elimination: \dfrac{\forall x \; \varphi}{\varphi[t/x]} \forall x \; \text{e}
\forallx introduction: To enclose \varphi in the scope of \forallx, we must prove \varphi being quantified for all possible values of x. If we can prove \varphi is true for an arbitrarily selected fresh x_0 in the universe, then we can claim \varphi is true for all x. It is written as: \dfrac{\boxed{\begin{array}{c}x_0 \; \; \; \; \; \; \; \; \; \; \; \; \; \; \\ \vdots \\ \varphi[x_0/x] \end{array}}}{\forall x \varphi} \forall x \; \; i The scope of x_0 is limited to the proof box: it is fresh, so that does not appear before we make the proof and will not be used after the proof.
\existsx introduction: \dfrac{\varphi[t/x]}{\exists x \varphi(x)} \exists x \; i
\existsx elimination: given a formula \existsx \varphi(x) and x_0, if assuming \varphi(x_0) is true we can prove a formula \mathcal{X}, then we claim that \mathcal{X} is true: \dfrac{\exists x \; \: \varphi(x), \boxed{\begin{array}{c}x_0 \; \; \; \; \varphi([x_0/x]) \\ \vdots \\ \mathcal{X} \end{array}}}{\mathcal{X}} \exists x \; e
2.6 Semantics of predicate logic
An interpretation provides semantic meaning to the terms and formulas of the language.
Variables are objects that form the domain of discourse D, the set of considered objects. The interpretation of a function symbol is a function.
Each function symbol f of arity n is assigned a function from D^n to D.
A constant symbol is a function symbol with 0 arguments (D^0 \rightarrow D).
The interpretation of an n-ary predicate symbol is a set of n-tuples of elements of the domain of discourse. Each predicate symbol P of arity n is assigned a relation I(P) over D^n or, equivalently, a function from D^n to {true, false}.
Let \mathcal{F} be a set of function symbols and \mathcal{P} a set of predicate symbols, each symbol with a fixed number of arguments. A model \mathcal{M} over the pair of (\mathcal{F}, \mathcal{P}) consists of:
A nonempty set D^M representing the domain of discourse
A concrete element f^M to D^M for every nullary function f \in \mathcal{F}
A concrete element f^M: (D^M)^n \rightarrow D^M for every n-ary (n > 0) function f \in \mathcal{F}
A subset P^M of n-tuples over D^M for every n-ary predicate P \in \mathcal{P}
A sentence \varphi is satisfiable if there is a model \mathcal{M} under which it evaluates to true. We also say that \mathcal{M} satisfies \varphi denoted by \mathcal{M} \vDash \varphi.
A formula is logically valid if it’s true in every possible model.